\begin{tabbing}
$\forall$\=$E$:Type, $T$, $V$:(Id$\rightarrow$Id$\rightarrow$Type), $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), ${\it pred?}$:($E$$\rightarrow$(?$E$)),\+
\\[0ex]${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id))), ${\it init}$:($i$:Id$\rightarrow$EState($T$($i$))),
\\[0ex]${\it Trans}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$EState($T$($i$))$\rightarrow$EState($T$($i$))),
\\[0ex]${\it val}$:($e$:$E$$\rightarrow$kindcase(kind($e$); $a$.$V$(loc($e$),$a$); $l$,$t$.$M$($l$,$t$) )), ${\it time}$:($E$$\rightarrow\mathbb{Q}$).
\-\\[0ex]($\forall$$e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ (loc(pred($e$)) = loc($e$) $\in$ Id))
\\[0ex]$\Rightarrow$ SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:$E$. state\_after($e$) $\in$ EState($T$(loc($e$))))
\end{tabbing}